es:ES, ds:x:Id fp Type, T:Type, i:Id, f:(State(ds)T).
(x, y:T. Dec(x = y))
 (x:Id. vartype(i;x)  ds(x)?Top)
 e'@i.
 (e<e'. f((state when e)) = f((state when e')))
  (e:E.
  ((e <loc e')
  (& f((state when e)) = f((state when e'))
  (& & (e'':E. (e <loc e'')  e''  e'   f((state when e'')) = f((state when e'))  T)) 

latex

Definitions

t  T, x:A. B(x), E, (e <loc e'), e  e' , P & Q, A & B, x:A. B(x), e<e'. P(e), P  Q, False, P  Q, A, loc(e), Id, Prop, first(e), , b, Top, IdDeq, x. t(x), f(x)?z, vartype(i;x), pred(e), P  Q, State(ds), state@i, (state when e), ES, a:A fp B(a), 1of(t), e@i. P(e), P  Q, Dec(P), T, True, {T}, SQType(T)

Lemmas

es-axioms, es-pred-locl, or functionality wrt iff, exists functionality wrt iff, cand functionality wrt iff, and functionality wrt iff, all functionality wrt iff, implies functionality wrt iff, es-le-iff, alle-lt wf, true wf, squash wf, es-loc-pred, decidable wf, decl-state wf, fpf wf, event system wf, alle-at-iff, es-locl wf, es-le wf, es-state-when wf, subtype rel dep function, subtype rel self, es-le-loc, es-locl-iff, es-pred wf, es-vartype wf, fpf-cap wf, id-deq wf, top wf, not wf, assert wf, es-first wf, Id wf, es-loc wf, es-E wf